Functional verification of digital hardware designs has become an important and resource-intensive aspect of the product design cycle. With the increasing size and complexity of designs, simulation-based validation is no longer sufficient to provide the requisite design coverage needed to expose subtle bugs. Formal verification techniques such as symbolic model checking based on binary decision diagrams offer the potential of exhaustive coverage. However, in practice, their application has been limited by the state explosion problem.